(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(l(x1)) → l(a(x1))
r(a(x1)) → a(r(x1))
b(l(x1)) → b(a(r(x1)))
r(b(x1)) → l(b(x1))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(l(z0)) → l(a(z0))
r(a(z0)) → a(r(z0))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))
Tuples:
A(l(z0)) → c(A(z0))
R(a(z0)) → c1(A(r(z0)), R(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
S tuples:
A(l(z0)) → c(A(z0))
R(a(z0)) → c1(A(r(z0)), R(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
K tuples:none
Defined Rule Symbols:
a, r, b
Defined Pair Symbols:
A, R, B
Compound Symbols:
c, c1, c2, c3
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
R(
a(
z0)) →
c1(
A(
r(
z0)),
R(
z0)) by
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(l(z0)) → l(a(z0))
r(a(z0)) → a(r(z0))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))
Tuples:
A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
S tuples:
A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
B(l(z0)) → c3(B(a(r(z0))), A(r(z0)), R(z0))
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
K tuples:none
Defined Rule Symbols:
a, r, b
Defined Pair Symbols:
A, R, B
Compound Symbols:
c, c2, c3, c1
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
B(
l(
z0)) →
c3(
B(
a(
r(
z0))),
A(
r(
z0)),
R(
z0)) by
B(l(a(z0))) → c3(B(a(a(r(z0)))), A(r(a(z0))), R(a(z0)))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(l(z0)) → l(a(z0))
r(a(z0)) → a(r(z0))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))
Tuples:
A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
B(l(a(z0))) → c3(B(a(a(r(z0)))), A(r(a(z0))), R(a(z0)))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
S tuples:
A(l(z0)) → c(A(z0))
R(b(z0)) → c2(B(z0))
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
B(l(a(z0))) → c3(B(a(a(r(z0)))), A(r(a(z0))), R(a(z0)))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
K tuples:none
Defined Rule Symbols:
a, r, b
Defined Pair Symbols:
A, R, B
Compound Symbols:
c, c2, c1, c3
(7) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
R(b(z0)) → c2(B(z0))
R(a(a(z0))) → c1(A(a(r(z0))), R(a(z0)))
R(a(b(z0))) → c1(A(l(b(z0))), R(b(z0)))
B(l(a(z0))) → c3(B(a(a(r(z0)))), A(r(a(z0))), R(a(z0)))
B(l(b(z0))) → c3(B(a(l(b(z0)))), A(r(b(z0))), R(b(z0)))
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(l(z0)) → l(a(z0))
r(a(z0)) → a(r(z0))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))
Tuples:
A(l(z0)) → c(A(z0))
S tuples:
A(l(z0)) → c(A(z0))
K tuples:none
Defined Rule Symbols:
a, r, b
Defined Pair Symbols:
A
Compound Symbols:
c
(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
A(l(z0)) → c(A(z0))
We considered the (Usable) Rules:none
And the Tuples:
A(l(z0)) → c(A(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(A(x1)) = [5]x1
POL(c(x1)) = x1
POL(l(x1)) = [1] + x1
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(l(z0)) → l(a(z0))
r(a(z0)) → a(r(z0))
r(b(z0)) → l(b(z0))
b(l(z0)) → b(a(r(z0)))
Tuples:
A(l(z0)) → c(A(z0))
S tuples:none
K tuples:
A(l(z0)) → c(A(z0))
Defined Rule Symbols:
a, r, b
Defined Pair Symbols:
A
Compound Symbols:
c
(11) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(12) BOUNDS(O(1), O(1))